Definitions | i j < k, rel_exp(T;R;n), R^+, {T}, x f y, R^*, P  Q, P  Q, eventlist(pred?;e), sends-bound(p;e;l), (x l), A B, False, i j, ||as||, eqof(d), l[i], {i..j }, receives(dE;dL;pred?;info;p;e;l), index(dE;dL;pred?;info;p;r), S T, rcv-from-on(dE;dL;info;e;l;r), , SWellFounded(R(x;y)), A & B, A, b, first(e), pred(e), EqDecider(T), x:A. B(x), sender(e), IdLnk, link(e), P & Q, P Q, e < e', destination(l),  x,y. t(x;y), pred!(e;e'), Id, loc(e), Unit, Prop, P  Q, rcv?(e), x:A. B(x), t T |